
\documentclass{article}
\usepackage{graphicx}
\usepackage{amsmath}
\usepackage{epstopdf}

\begin{document}

\title{Performance Analysis : PRISM}
\author{Floris van Nee, Simon Dirlik and Maarten Meijer}

\maketitle

\section{Exercise 1}
\subsection{}
	When we generate random paths through the model,
	the size of the queue never gets above 1 because the serve rate is much higher than the arrival rate.

\subsection{}
	When more requests arrive while the queue is full, the queue remains the maximum value (20)
	and the additional requests are ignored.

\subsection{}
	The size of the state space of this model is 21.

\subsection{}
	The steady-state distributions of the system are given in table \ref{table:SQssd}.
	The steady state distributions are: $\frac {1} {2^{q+1}}$, where q is the number of messages in the queue.
	\begin{table}[h]
		\begin{center}
			\begin{tabular}{ | l  | l | l | }
				\hline
						&	20 					&	100			\\ \hline\hline
				0		&	0.5000002362003579	&	0.5			\\ \hline
				1		&	0.250000118321174	&	0.25		\\ \hline
				2		&	0.12500005938158212	&	0.125		\\
				\hline
			\end{tabular}
			\caption{Steady-state distributions for q\_max is 20 and 100, with 0, 1 and 2 messages in the queue}
			\label{table:SQssd}
		\end{center}
	\end{table}

\subsection{}
	The CSL property that the probability of the queue being empty at time t is greater than 50\% is:
	\begin{verbatim}
	P>0.5 [ F[t,t](q=0) ]
	\end{verbatim}
	This property verifies in PRISM.

\subsection{}
	The probability for arbitrary $t$ can be found with the following formula:
	\begin{verbatim}
	P=? [ F[t,t](q=0) ]
	\end{verbatim}
	Evaluating an experiment in PRISM with this formula for $t$ ranging from 0 to 10 results in figure \ref{fig:1.6}. To calculate the value that this probability converges to for large $t$, the steady-state probability needs to be calculated. This can be done with the following formula: \verb|S=? [q=0]|. Evaluating this is PRISM leads to the steady-state probability 0.5. This is the value that the probability converges to as $t$ goes to infinity.
	\begin{figure}[htbp]
		\centering
			\includegraphics[width=1.00\textwidth]{img/1_6.eps}
		\caption{The plot for the probability 'the probability that the queue is empty at time t' for t ranging from 0 to 10}
		\label{fig:1.6}
	\end{figure}
	
\subsection{}
	This property can be specified as follows:
	\begin{verbatim}
	P<0.05 [ F<10 q=q_max ]
	\end{verbatim}
\subsection{}
	Plotting the property of the previous question for different values of q\_max leads to figure \ref{fig:1.8}. Because it has a logarithmic scale on the y-axis and it still grows faster than a straight line, the function converges superexponentially. Therefore, the probability of the property converges to zero as q\_max grows, which causes the property that the probability is smaller than 5\% to always hold for large values of q\_max.
\clearpage
	\begin{figure}[htbp]
		\centering
			\includegraphics[width=1.00\textwidth]{img/1_8.eps}
		\caption{The plot for the probability 'the probability that the buffer has become full at some time point before time t = 10' for different q\_max}
		\label{fig:1.8}
	\end{figure}
\subsection{}
	The number of dropped messages can be tracked by specifying the following reward in the model:
	\begin{verbatim}
	rewards "messages_dropped"
		 [request] q=q_max : 1;
	endrewards
	\end{verbatim}
	This will give a reward of one every time a request occurs when the queue is full. Then the following properties can be used to check the dropped messages:
	\begin{verbatim}
	R{"messages_dropped"}=? [C<=t]
	R{"messages_dropped"}=? [F(q=0)]
	\end{verbatim}
	The first property calculates the number of dropped messages until time $t$. The second property calculates the number of dropped messages until the queue is empty.
\subsection{}
	The property to calculate this number of dropped messages was already given in the previous answer, but is repeated here for convenience:
	\begin{verbatim}
	R{"messages_dropped"}=? [F(q=0)]
	\end{verbatim}
	The plot of this for values of q\_max ranging from 2 to 20 can be found in figure \ref{fig:1.10}. Also, to show that it is exponential, the plot with a logarithmic y-as is shown in figure \ref{fig:1.10a}. Because the figure consists of a straight line with logarithmic y-axis, the function decreases exponentially.
	\begin{figure}[htbp]
		\centering
			\includegraphics[width=1.00\textwidth]{img/1_10.eps}
		\caption{The plot for the expected number of dropped messages before the queue is empty versus different values of q\_max}
		\label{fig:1.10}
	\end{figure}
	
	\begin{figure}[htbp]
		\centering
			\includegraphics[width=1.00\textwidth]{img/1_10a.eps}
		\caption{The plot for the expected number of dropped messages before the queue is empty versus different values of q\_max on a logarithmic scale}
		\label{fig:1.10a}
	\end{figure}
\section{Exercise 2}

\subsection{}
	A PRISM model that models the different cars with a full message queue is created. The essentials of the model can best be described by the state chart given in figure \ref{fig:statechart}. Here, whenever a message is sent, a non-deterministic backoff state is entered. To indicate that a message is send, the variable \texttt{sendA} is set whenever state zero will be reached.
\\
	\begin{figure}[here]
		\begin{center}
			\includegraphics[width=10cm, clip=true, trim=0 19.5cm 5cm 4.6cm]{../assignment2/statechart.pdf}
			\caption{Statechart of backoff phase}
			\label{fig:statechart}
		\end{center}
	\end{figure}

The probability matrix describing the transition from backoff state zero is implemented flexible such that the probability matrix is valid for a number of cars \textit{W} up to 21 (i.e. \textit{W}=20). Hereby, the transition from backoff phase zero to a new backoff phase is formed by a summation of the following form:
	\begin{equation}
	( W\,>\,w_n\,?\,1\,:\,0 ) * 1/W: (backoffA'=w_n) + ... 
	\end{equation}
	Where $w_n$ takes values from $0$ to $W-1$. An advantage of this is that it is easier to change the backoff number, because it remains valid for any number up to 21. For numbers larger than 21, more of these lines have to be added. Of course, it could have also been written in the form without the conditional expression, however this would require the number of lines to changes for every change of the backoff number.
	\\ \\
	To add an extra car to the model, a new line has to be added that renames the module for car A with this newly added car, i.e.:
	\begin{verbatim}
	module carX = carA[backoffA=backoffX] endmodule
	\end{verbatim}

\subsection{}
	Whenever a particular car is in backoff state zero, it will send the first message in the queue. Whenever an other car sends its message at the same time, a collision has occured and no car will receive the message correctly. The probability that a successful transmission has occurred within \textit{k} time slots can be described using the following pCTL property:
	\begin{verbatim}
	P>0.10 [ F<10 (sendA + sendB + sendC = 1) ]
	\end{verbatim}
	Where \textit{k} is fixed to 10 and the probability must be greater then 10\%. This properties states that at least one car is eventually sending in \textit{k} steps.

\subsection{}
	The property of (2) can be used to plot the probability for variable k. In figure \ref{fig:exercise2-3} the probability of a successful transmission for a variable number of steps \textit{k} is plotted. \\
	\begin{figure}[here]
		\begin{center}
			\includegraphics[width=12cm, clip=true, trim=0 15.3cm 0cm 4.6cm]{../assignment2/excercise2.pdf}
			\caption{Probability of a successful transmission for variable k with fixed W and n. (respectively 8 and 3)}
			\label{fig:exercise2-3}
		\end{center}
	\end{figure}
\subsection{}
	In order to compute the number of collisions and successful transmissions two reward structures are defined, named \textit{``successfultransmission''} and \textit{``collision''} respectively. The reward expressions are given by:
	\begin{verbatim}
	sendA + sendB + sendC = 1 : 1;
	sendA + sendB + sendC > 1 : 1;
	\end{verbatim} 
	The length of these expressions will grow linearly with n.
\subsection{}
	The property that the steady-state probability that a collision occurs during a time slot is greater than 5\% can be expressed using PRISM's reward language using:
	\begin{verbatim}
	R{"collision"}>0.05 [ S ]
	\end{verbatim}
	Where the ``collision'' reward is defined in the model as:
	\begin{verbatim}
	rewards "collision"
		sendA + sendB + sendC > 1 : 1;
	endrewards
	\end{verbatim}
\subsection{}
	On average, it is given that there are about 7.9239 time slots between each pair of collisions. This can be calculated by using the steady state probability that a collision occurs. Now, however, we are not interested in the average proportion of a time step that corresponds to a collision, which can be calculated with the following PRISM steady state property:
	\begin{verbatim}
	1 / S=? [ (sendA+sendB+sendC>1) ]  =>  7.9239
	\end{verbatim}

\subsection{}
	\label{subsec:collisionreward}
	The property that the expected number of collisions after $k$ time slots is greater than 3 can be specified as follows using PRISM’s reward language:
	\begin{verbatim}
	R{"collision"}>3 [ C<=k ]
	\end{verbatim}
\subsection{}
	The expected number of collisions for varying $k$ is calculated using the property of \ref{subsec:collisionreward} and is displayed in figure \ref{fig:exercise10}. In the figure, it can be seen that the expected number of collisions for low $k$ is slowly increasing, this is caused by the fact that all cars have a full queue and start simultaniously sending at $k=1$ and start entering the backoff phase together. Thereafter, this effect is middled out and the slope of the graph approaches the steady state probability of collisions.
	\begin{figure}[here]
		\begin{center}
			\includegraphics[width=12cm, clip=true, trim=0 16.3cm 0cm 4.6cm]{../assignment2/excercise10.pdf}
			\caption{The expected number of collisions for variable k with fixed W and n. (respectively 8 and 3)}
			\label{fig:exercise10}
		\end{center}
	\end{figure}
\section{Exercise 3}

\subsection{}
	The expected value of a exponentially distributed variable is $\frac{1}{\lambda}$. The expected time for message arrival is $\frac{1}{20}$, as specified in the exercise. Then, $\lambda$ is $\frac{1}{\frac{1}{20}} = 20$.
	\[
	P(X<t)=1-P(X>t)=1- e^{-\lambda t} = 1 - e^{-20 \cdot 0.016} \approx 0.2739
	\]

\subsection{}
	In this step, the idea is to remove the assumption that there are always messages to be transmitted and provide a service queue in which messages to be send can be queued. To do this, a slightly modified version of the service queue of the first exercise was added to the model. Every car has one queue, and every queue has two variables: \verb|done| and \verb|q|. The variable \verb|q| specifies how many messages there are in the queue. The variable \verb|done| specifies the state of the model. If \verb|done| is 0, the request transition is enabled, allowing every queue to add a message to the queue with probability 0.2739. Also, messages can be served now, which will put the car in a state where it is transmitting. When every queue has had a request transition, and the serve transition is taken when needed, lastly the step transition will be taken. This transition acts as the transition to the next time slot.\\
	Because, in our model, time only advances in the step transition, we are only interested in this step transition when looking at rewards. Therefore, the rewards need to be synchronized on the step transition.\\
	In our model, we did not make the second, rather strange, assumption that the backoff of cars does not decrease when other cars are transmitting. This decision was made, because we felt this would come closer to reality. Of course, if you know when other cars are transmitting, you can avoid collisions altogether. Therefore, we extended the model to the point where backoffs are always decreased, also when other cars are transmitting. If it is really needed to obtain the behavior as specified with the assumption, the following two lines can be added to the model in the car module, instead of the line which normally decreases the backoff:
	\begin{verbatim}
		[step] done=1 & backoffA>0 & (sendA+sendB+sendC>0) ->
				 1: (backoffA'=backoffA);
		[step] done=1 & backoffA>0 & (sendA+sendB+sendC=0) ->
				 1: (backoffA'=backoffA-1);
	\end{verbatim}
	The complete model can be found in assignment3/dtmc\_carmodel.pm.
	The model can be validated using the fact that the addition of the steady-state probabilities for successful transmission, collision and radio silence sums to one. To realize this, reward structures for these properties are added. Then, the probabilities can be calculated using the following properties:
	\begin{equation}
	\frac{R\{``successfultransmission"\}=? [ S ]}{S=? [ ``step" ]}
	\end{equation}
	\begin{equation}
	\frac{R\{``collision"\}=? [ S ]}{S=? [ ``step" ]}
	\end{equation}
	\begin{equation}
	\frac{R``\{radiosilence"\}=? [ S ]}{S=? [ ``step" ]}
	\end{equation}
	where the label ``step'' is defined as:
	\begin{verbatim}
	step := done=0 & doneB=0 & doneC=0 & sendA=0 & sendB=0 & sendC=0
	\end{verbatim}
	Thus, the steady state probability for a certain reward are divided by the steady state probability that the model is in the `step' action.\\
	Evaluation of these properties leads to the following results:
	\begin{equation}
	\label{eq:steadystates}
		\begin{split}
			S(succesfull\,transmission) & = 36.2 \%\\
			S(collision)				& = 8.5 \%\\
			S(radio\,silence)			& = 55.3 \%\\
		\end{split}
	\end{equation}
	Which indeed sums nicely to one.
	For each car i, the steady-state probability $\tau_i$ is defined as the probability that car i is transmitting, which can again be calculated using rewards.  For n=3 and W=8 $\tau_i$ evaluates to 17.9\%. Note that successful transmission (eq \ref{eq:steadystates}) can also be calculated using $\tau$:
	\begin{equation}
	S(succesfull\,transmission) = 3 * 0.179*(1-0.179)^2 = 0.362
	\end{equation}
	% Why multiply by 3? This seems to be wrong
	% answer: Because there are 3 cars that can each send without collision
\subsection{}
	The state space for ten cars is very large, approximately $200\cdot 10^{15}$. Because of the large state space it is not possible to compute the steady-state probability for this model. When trying to determine thiis probability, PRISM complains about not having enough memory available to do the calculation.
\subsection{}
	When $\tau_2$ and $\tau_3$ are given, the probability that car 1 can count down its backoff timer is: $(1-\tau_2)\cdot(1-\tau_3)$
\subsection{}
	In a DTMC that models 1 car and assumes that $\tau_2=\tau_3=1/2$, $\tau_1=0.0644$.%0.06443164257510499
\subsection{}
	In exercise 3.5 we see that $\tau_1$ and $\tau_2$ are not equal.
	Instead of trying different values for $\tau_i$, $\tau_1$ was plotted against $\tau_2=\tau_3=[0..1]$, with step 0.01.
	This graph was exported to a matlab file (assignment3/tau\_n3.m) and using matlab the line $\tau_1=\tau_2=\tau_3$ was plotted in the same graph.
	The needed value is where the lines intersect.
	Figure \ref{fig:taun3} shows that $\tau_i=0.1488$.
	This is slightly lower than the value found in exercise 3.2,
	however this comparison is not useful because our implementation of the model does not include the assumption that the backoff does not decrease when other cars are transmitting.
	\begin{figure}[htbp]
		\centering
			\includegraphics[width=0.9\textwidth]{img/tau_n3.eps}
		\caption{The plot showing the intersection of $\tau_1=\tau_2=\tau_3$ for n=3}
		\label{fig:taun3}
	\end{figure}
\subsection{}
	The same method was used to find this value, the matlab file is in assignment3/tau\_n10.m.
	Figure \ref{fig:taun10} shows that for $n=10$, $\tau_i=0.0965$.
	The probability that one of the cars is transmitting is $\tau_1=\tau_2=\tau_3$.\\
	\begin{figure}[htbp]
		\centering
			\includegraphics[width=0.9\textwidth]{img/tau_n10.eps}
		\caption{The plot showing the intersection of $\tau_1=\tau_2=\tau_3$ for n=10}
		\label{fig:taun10}
	\end{figure}\\
	A collision occurs in one of the following cases:\\
	car 1 and 2 are transmitting and car 3 is not transmitting or\\
	car 1 and 3 are transmitting and car 2 is not transmitting or\\
	car 2 and 3 are transmitting and car 1 is not transmitting or\\
	all cars are transmitting.\\
	This translates to the following equation:
	\begin{equation}
		S(collision) = 3*(0.0965^2)*(1-0.0965)+(0.0965^3) = 0.026139486
	\end{equation}
	This can also be calculated as follows:
	\begin{equation}
		\begin{split}
			S(succesfull\,transmission)	& = 3 \cdot 0.0965 \cdot (1-0.0965)^2 = 0.236322396\\
			S(radio\,silence)			& = (1-0.0965)^3 = 0.737538118\\
			S(collision)				& = 1 - S(succesfull\,transmission) - S(radio\,silence)\\
										& = 1 - 0,236322396 - 0.737538118\\
										& = 0.026139486\\
		\end{split}
	\end{equation}

\end{document}
